Lean Forward 2019
Загальні враження
По-перше хочу подякувати усім, хто мене підтримує, надихає та прощає мені багато чого. Попасти на таку подію — це справжній подарунок та задоволення від усвідомлення, що коло однодумців більше, ніж ти очікував. Назвичайно був вражений теплим сердечним прийомом та щирим і відкритим інтерв'ю Хенка Барендрехта, перша частина якого опублікована в інстаграмі, а друга на ютубі та фейсбуці. Хенк Барендрехт відомий нам інженерам як автор лямбда кубу, цілої системи формальних моделей які поєднують та класифікують усі лямбда числення в залежності від різного набору чотирьох формул * : *, * : ☐, ☐ : ☐, ☐ : *. Фактично, усі типизовані мови програмування, включаючи PTS (CoC, System Pω, або чиста система), яка є ядром усіх пруверів, потрапляють у лямбда куб. До цього Хенк Барендрехт також повністю формалізував та довів майже усі теореми про нетипизоване лямбда числення яке теж є основою багатьох мов з динамічною типизацією. Його український учень Андрій Полонський, який повернувся в Україну під час Майдану, довів спростування кон'юнктури Хенка Барендрехта, яке лягло в основу сучасних ідей оптимальної бета-редукції, яка була реалізована в роботах Антона Саліхметова та Майя Віктора (мова Formality з залежними індуктивними типами, написана на Rust, містить оптимальний евалуатор бета-редукцій та здійснює екстракт в GPU).
Хенк зараз досліджує свідомість за допомогою формальних методів та медитації, він є сертифікованим учителем Віпаш'яни в стилі Махасі, його учителями були Кобун Чіно Роші та Фра Меттавіхарі. Найближчі його ретріти в 2019 році в Греції та Італії. Хенк також пише статті на тему формальної філософії, формалізації буддійських систем та формалізації свідомості. Можливо варто спробувати написати огляд робіт Хенка для нашого каналу Формальної Філософії, якщо кількість підписників, скажімо, подвоїться.
Враження від доповідей
Найбільше мене зацікавили наступні доповіді:
Jeremy Avigad
Перша — Джеремі Авігада по факторизації поліноміальних функторів. В секції питань його запитали чи дійсно дійсні числа закодовані як фактор-типи коіндуктивних послідовностей цифр є найкрасивішою моделлю дійсних чисел і Джеремі відповів, шо так. Репозиторій https://github.com/avigad/qpf та слайди презентації.
class qpf (F : Type u → Type u) [functor F] :=
(P : pfunctor.{u})
(abs : Π {α}, P.apply α → F α)
(repr : Π {α}, F α → P.apply α)
(abs_repr :∀ {α} (x:Fα), abs(reprx)=x)
(abs_map : ∀ {α β} (f : α → β) (p : P.apply α),
abs (f <$> p) = f <$> abs p)
Reid Barton
Друга — Ріда Бартона по формалізації модель-категорій Квілена та структурі моделі Квілена на топологічному просторі. У цій роботі розглянутий трансфінітний випадок, проведена велика класифікація топологічних просторів (найбільша на моїй пам'яті), достатньо пророблена теорія категорій та фундаментальний групоїд, категорія корозшарувань, факторизація Брауна. Репозиторій на гітхабі: https://github.com/rwbarton
class model_category (M : Type u) extends category.{u v} M :=
(complete : has_limits M)
(cocomplete : has_colimits M)
(W C F : morphism_class M)
(h : is_model_category W C F)
structure is_model_category (W C F : morphism_class M) : Prop :=
(weq : is_weak_equivalences W)
(caf : is_wfs C (F ∩ W))
(acf : is_wfs (C ∩ W) F)
def Meas : Type (u+1) := bundled measurable_space
def Top : Type (u+1) := bundled topological_space
def Borel : Top ⥤ Meas :=
concrete_functor @measure_theory.borel
@measure_theory.measurable_of_continuous
instance (x : Top) : topological_space x := x.str
instance (x : Meas) : measurable_space x := x.str
instance : concrete_category @measurable :=
⟨@measurable_id, @measurable.comp⟩
instance : concrete_category @continuous :=
⟨@continuous_id, @continuous.comp⟩
Jesse Han
Третя — доведення незалежності континуум гіпотези від Джесі Хана. Джесі Хана також цікавить транспорт з топоса в класичну топологію. Його код та презинтація представлені гітхаб організацією https://github.com/flypitch
theorem independence_of_CH :
(¬ ZFC ⊢' continuum_hypothesis)
∧ (¬ ZFC ⊢' ∼ continuum_hypothesis) :=
begin
have := CH_consistent,
have := neg_CH_consistent, repeat{auto_cases},
apply @independence_of_exhibit_models L_ZFC ZFC
ZFC_consistent continuum_hypothesis,
show Model ZFC,
exact this_w_1,
show Model ZFC,
exact this_w,
repeat{assumption}
end
Далі буде.